T:Type, x, y:(Top List). (null(x))  (null(y))  (x = y  (T List)) 

latex

Definitions	False, t  T, x:A. B(x), P  Q, True, type List, [], b, Top, x:AB(x), s = t, Type
Lemmas	top wf, true wf, false wf